RewriteNondeterministic.agda:19,9-13
c != b of type A
when checking that the expression refl has type f a ≡ b
